Nuprl Lemma : Q-R-glues_functionality 11,40

es:ES, R:(EE), AB:Type, Ia:AbsInterface(A), Ib:AbsInterface(B), f:(E(Ia)B), Q1,
Q2:(EE), g:(E(Ib)E).
Q1  Q2  (g glues Ia:Q1 f Ib:R  g glues Ia:Q2 f Ib:R
latex


Definitions{I}, f is Q-R-pre-preserving on P, x:AB(x), x:A  B(x), b, ES, x:AB(x), Type, AbsInterface(A), P  Q, R1  R2, s = t, Q ==f== P, Q f== P, f(a), Inj(A;B;f), A c B, P & Q, g glues Ia:Qa f Ib:Rb, t  T, EState(T), Id, , pred!(e;e'), SWellFounded(R(x;y)), Unit, Void, x:A.B(x), Top, S  T, left + right, suptype(ST), first(e), A, loc(e), <ab>, P  Q, constant_function(f;A;B), IdLnk, x,yt(x;y), xt(x), kindcase(ka.f(a); l,t.g(l;t) ), Knd, , r  s, e < e', val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), , Msg(M), type List, kind(e), EOrderAxioms(Epred?info), EqDecider(T), , E, e  X, {x:AB(x)} , E(X), let x,y = A in B(x;y), t.1, P  Q, x:AB(x), t  ...$L, R1  R2, P1  P2, {T}, True, T, SqStable(P), s ~ t, SQType(T)
Lemmassq stable from decidable, decidable assert, weak-antecedent-surjection-property, Q-R-pre-preserving functionality wrt implies, predicate implies weakening, predicate equivalent weakening, rel implies weakening, rel equivalent inversion, rel equivalent weakening, es-interface-predicate wf, subtype rel sum, Q-R-glues wf, iff wf, rel equivalent wf, subtype rel function, es-E-interface wf, es-is-interface wf, es-E wf, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, assert wf, first wf, top wf, unit wf, event system wf

origin